(set-logic QF_LRA)
(set-info :source |
Fully parameterized specification and verification of a synchronizer   
circuit modeling metastability at various levels of refinement.     
A paper describing this specification, to be published in Designing     
Correct Circuits (DCC), 2006, is available from the authors.            

Geoffrey Brown, Indiana University <geobrown@cs.indiana.edu>
Lee Pike, Galois Connections, Inc. <leepike@galois.com>

Translated into CVC format by Leonardo de Moura.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun x_0 () Bool)
(declare-fun x_1 () Bool)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Bool)
(declare-fun x_5 () Bool)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Bool)
(declare-fun x_9 () Bool)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Bool)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Bool)
(declare-fun x_17 () Bool)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Bool)
(declare-fun x_31 () Bool)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Bool)
(declare-fun x_37 () Bool)
(declare-fun x_38 () Bool)
(declare-fun x_39 () Bool)
(declare-fun x_40 () Bool)
(declare-fun x_41 () Real)
(declare-fun x_42 () Bool)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Bool)
(declare-fun x_53 () Real)
(declare-fun x_54 () Bool)
(declare-fun x_55 () Bool)
(declare-fun x_56 () Real)
(declare-fun x_57 () Bool)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Real)
(declare-fun x_64 () Real)
(declare-fun x_65 () Real)
(declare-fun x_66 () Bool)
(declare-fun x_67 () Real)
(declare-fun x_68 () Bool)
(declare-fun x_69 () Bool)
(declare-fun x_70 () Real)
(declare-fun x_71 () Bool)
(declare-fun x_72 () Real)
(declare-fun x_73 () Real)
(declare-fun x_74 () Real)
(declare-fun x_75 () Real)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Bool)
(declare-fun x_81 () Real)
(declare-fun x_82 () Bool)
(declare-fun x_83 () Bool)
(declare-fun x_84 () Real)
(declare-fun x_85 () Bool)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Real)
(declare-fun x_91 () Real)
(declare-fun x_92 () Real)
(declare-fun x_93 () Real)
(declare-fun x_94 () Bool)
(declare-fun x_95 () Real)
(declare-fun x_96 () Real)
(declare-fun x_97 () Bool)
(declare-fun x_98 () Bool)
(declare-fun x_99 () Bool)
(declare-fun x_100 () Bool)
(declare-fun x_101 () Real)
(declare-fun x_102 () Bool)
(declare-fun x_103 () Real)
(declare-fun x_104 () Real)
(declare-fun x_105 () Real)
(declare-fun x_106 () Real)
(assert (let ((?v_58 (= x_20 x_21)) (?v_59 (= x_22 x_23)) (?v_60 (= x_24 x_25)) (?v_56 (= x_26 x_27))) (let ((?v_61 (not ?v_56)) (?v_64 (= x_28 x_29)) (?v_53 (= x_30 x_31)) (?v_54 (= x_7 x_3)) (?v_57 (ite (<= x_22 x_26) x_22 x_26)) (?v_52 (ite (<= x_26 x_22) x_26 x_22)) (?v_45 (= x_47 x_20)) (?v_46 (= x_23 x_48)) (?v_47 (= x_49 x_24)) (?v_43 (= x_27 x_50))) (let ((?v_48 (not ?v_43)) (?v_51 (= x_51 x_28)) (?v_40 (= x_52 x_30)) (?v_41 (= x_11 x_7)) (?v_44 (ite (<= x_23 x_27) x_23 x_27)) (?v_39 (ite (<= x_27 x_23) x_27 x_23)) (?v_32 (= x_61 x_47)) (?v_33 (= x_48 x_62)) (?v_34 (= x_63 x_49)) (?v_30 (= x_50 x_64))) (let ((?v_35 (not ?v_30)) (?v_38 (= x_65 x_51)) (?v_27 (= x_66 x_52)) (?v_28 (= x_15 x_11)) (?v_31 (ite (<= x_48 x_50) x_48 x_50)) (?v_26 (ite (<= x_50 x_48) x_50 x_48)) (?v_19 (= x_75 x_61)) (?v_20 (= x_62 x_76)) (?v_21 (= x_77 x_63)) (?v_17 (= x_64 x_78))) (let ((?v_22 (not ?v_17)) (?v_25 (= x_79 x_65)) (?v_14 (= x_80 x_66)) (?v_15 (= x_19 x_15)) (?v_18 (ite (<= x_62 x_64) x_62 x_64)) (?v_13 (ite (<= x_64 x_62) x_64 x_62)) (?v_6 (= x_89 x_75)) (?v_7 (= x_76 x_90)) (?v_8 (= x_91 x_77)) (?v_4 (= x_78 x_92))) (let ((?v_9 (not ?v_4)) (?v_12 (= x_93 x_79)) (?v_1 (= x_94 x_80)) (?v_2 (= x_95 x_19)) (?v_5 (ite (<= x_76 x_78) x_76 x_78)) (?v_0 (ite (<= x_78 x_76) x_78 x_76)) (?v_3 (= x_98 x_17)) (?v_11 (= x_19 x_95)) (?v_16 (= x_17 x_13)) (?v_24 (= x_15 x_19)) (?v_29 (= x_13 x_9)) (?v_37 (= x_11 x_15)) (?v_42 (= x_9 x_5)) (?v_50 (= x_7 x_11)) (?v_55 (= x_5 x_1)) (?v_63 (= x_3 x_7))) (let ((?v_10 (+ ?v_5 x_34)) (?v_23 (+ ?v_18 x_34)) (?v_36 (+ ?v_31 x_34)) (?v_49 (+ ?v_44 x_34)) (?v_62 (+ ?v_57 x_34))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (> x_32 0) (> x_33 0)) (>= x_34 0)) (< x_34 x_32)) (< x_34 x_33)) (>= x_45 0)) (< x_45 x_32)) (< x_45 x_33)) (or (= x_16 x_17) (= x_18 x_19))) (or (= x_12 x_13) (= x_14 x_15))) (or (= x_8 x_9) (= x_10 x_11))) (or (= x_4 x_5) (= x_6 x_7))) (or (= x_0 x_1) (= x_2 x_3))) (or (and (and (and (and (and (and (and (and (and (= x_96 0) (= x_97 x_85)) (= ?v_0 x_78)) (<= (+ ?v_0 x_32) x_92)) (or ?v_3 (= x_98 x_16))) (= x_99 x_82)) (= x_100 x_83)) (= x_90 x_76)) ?v_1) ?v_2) (and (and (and (and (and (and (and (and (and (= x_96 1) (= x_100 x_82)) (= ?v_0 x_76)) (<= (+ ?v_0 x_33) x_90)) (or (and (and (= x_101 0) ?v_1) ?v_2) (and (and (= x_101 1) (= x_80 x_83)) (= x_94 (not x_80))))) (= x_102 x_85)) (= x_97 x_16)) (= x_103 x_18)) (= x_92 x_78)) ?v_3))) (or (or (and (and (and (= x_104 0) ?v_9) (or (not (<= x_75 ?v_5)) (= x_102 x_80))) ?v_6) (and (and (and (= x_104 1) ?v_4) (xor x_80 x_94)) (= x_89 ?v_10))) (and (and (and (= x_104 2) ?v_4) (= x_80 x_94)) ?v_6))) (or (or (and (and (and (= x_105 0) (not ?v_7)) (or (not (<= x_77 ?v_0)) (= x_99 x_17))) ?v_8) (and (and (and (= x_105 1) ?v_7) (xor x_17 x_98)) (= x_91 (+ ?v_0 x_45)))) (and (and (and (= x_105 2) ?v_7) (= x_17 x_98)) ?v_8))) (or (or (and (and (and (= x_106 0) ?v_9) (or (not (<= x_79 ?v_5)) (= x_103 x_19))) ?v_12) (and (and (and (= x_106 1) ?v_4) (not ?v_11)) (= x_93 ?v_10))) (and (and (and (= x_106 2) ?v_4) ?v_11) ?v_12))) (or (and (and (and (and (and (and (and (and (and (= x_81 0) (= x_16 x_71)) (= ?v_13 x_64)) (<= (+ ?v_13 x_32) x_78)) (or ?v_16 (= x_17 x_12))) (= x_82 x_68)) (= x_83 x_69)) (= x_76 x_62)) ?v_14) ?v_15) (and (and (and (and (and (and (and (and (and (= x_81 1) (= x_83 x_68)) (= ?v_13 x_62)) (<= (+ ?v_13 x_33) x_76)) (or (and (and (= x_84 0) ?v_14) ?v_15) (and (and (= x_84 1) (= x_66 x_69)) (= x_80 (not x_66))))) (= x_85 x_71)) (= x_16 x_12)) (= x_18 x_14)) (= x_78 x_64)) ?v_16))) (or (or (and (and (and (= x_86 0) ?v_22) (or (not (<= x_61 ?v_18)) (= x_85 x_66))) ?v_19) (and (and (and (= x_86 1) ?v_17) (xor x_66 x_80)) (= x_75 ?v_23))) (and (and (and (= x_86 2) ?v_17) (= x_66 x_80)) ?v_19))) (or (or (and (and (and (= x_87 0) (not ?v_20)) (or (not (<= x_63 ?v_13)) (= x_82 x_13))) ?v_21) (and (and (and (= x_87 1) ?v_20) (xor x_13 x_17)) (= x_77 (+ ?v_13 x_45)))) (and (and (and (= x_87 2) ?v_20) (= x_13 x_17)) ?v_21))) (or (or (and (and (and (= x_88 0) ?v_22) (or (not (<= x_65 ?v_18)) (= x_18 x_15))) ?v_25) (and (and (and (= x_88 1) ?v_17) (not ?v_24)) (= x_79 ?v_23))) (and (and (and (= x_88 2) ?v_17) ?v_24) ?v_25))) (or (and (and (and (and (and (and (and (and (and (= x_67 0) (= x_12 x_57)) (= ?v_26 x_50)) (<= (+ ?v_26 x_32) x_64)) (or ?v_29 (= x_13 x_8))) (= x_68 x_54)) (= x_69 x_55)) (= x_62 x_48)) ?v_27) ?v_28) (and (and (and (and (and (and (and (and (and (= x_67 1) (= x_69 x_54)) (= ?v_26 x_48)) (<= (+ ?v_26 x_33) x_62)) (or (and (and (= x_70 0) ?v_27) ?v_28) (and (and (= x_70 1) (= x_52 x_55)) (= x_66 (not x_52))))) (= x_71 x_57)) (= x_12 x_8)) (= x_14 x_10)) (= x_64 x_50)) ?v_29))) (or (or (and (and (and (= x_72 0) ?v_35) (or (not (<= x_47 ?v_31)) (= x_71 x_52))) ?v_32) (and (and (and (= x_72 1) ?v_30) (xor x_52 x_66)) (= x_61 ?v_36))) (and (and (and (= x_72 2) ?v_30) (= x_52 x_66)) ?v_32))) (or (or (and (and (and (= x_73 0) (not ?v_33)) (or (not (<= x_49 ?v_26)) (= x_68 x_9))) ?v_34) (and (and (and (= x_73 1) ?v_33) (xor x_9 x_13)) (= x_63 (+ ?v_26 x_45)))) (and (and (and (= x_73 2) ?v_33) (= x_9 x_13)) ?v_34))) (or (or (and (and (and (= x_74 0) ?v_35) (or (not (<= x_51 ?v_31)) (= x_14 x_11))) ?v_38) (and (and (and (= x_74 1) ?v_30) (not ?v_37)) (= x_65 ?v_36))) (and (and (and (= x_74 2) ?v_30) ?v_37) ?v_38))) (or (and (and (and (and (and (and (and (and (and (= x_53 0) (= x_8 x_42)) (= ?v_39 x_27)) (<= (+ ?v_39 x_32) x_50)) (or ?v_42 (= x_9 x_4))) (= x_54 x_37)) (= x_55 x_39)) (= x_48 x_23)) ?v_40) ?v_41) (and (and (and (and (and (and (and (and (and (= x_53 1) (= x_55 x_37)) (= ?v_39 x_23)) (<= (+ ?v_39 x_33) x_48)) (or (and (and (= x_56 0) ?v_40) ?v_41) (and (and (= x_56 1) (= x_30 x_39)) (= x_52 (not x_30))))) (= x_57 x_42)) (= x_8 x_4)) (= x_10 x_6)) (= x_50 x_27)) ?v_42))) (or (or (and (and (and (= x_58 0) ?v_48) (or (not (<= x_20 ?v_44)) (= x_57 x_30))) ?v_45) (and (and (and (= x_58 1) ?v_43) (xor x_30 x_52)) (= x_47 ?v_49))) (and (and (and (= x_58 2) ?v_43) (= x_30 x_52)) ?v_45))) (or (or (and (and (and (= x_59 0) (not ?v_46)) (or (not (<= x_24 ?v_39)) (= x_54 x_5))) ?v_47) (and (and (and (= x_59 1) ?v_46) (xor x_5 x_9)) (= x_49 (+ ?v_39 x_45)))) (and (and (and (= x_59 2) ?v_46) (= x_5 x_9)) ?v_47))) (or (or (and (and (and (= x_60 0) ?v_48) (or (not (<= x_28 ?v_44)) (= x_10 x_7))) ?v_51) (and (and (and (= x_60 1) ?v_43) (not ?v_50)) (= x_51 ?v_49))) (and (and (and (= x_60 2) ?v_43) ?v_50) ?v_51))) (or (and (and (and (and (and (and (and (and (and (= x_35 0) (= x_4 x_36)) (= ?v_52 x_26)) (<= (+ ?v_52 x_32) x_27)) (or ?v_55 (= x_5 x_0))) (= x_37 x_38)) (= x_39 x_40)) (= x_23 x_22)) ?v_53) ?v_54) (and (and (and (and (and (and (and (and (and (= x_35 1) (= x_39 x_38)) (= ?v_52 x_22)) (<= (+ ?v_52 x_33) x_23)) (or (and (and (= x_41 0) ?v_53) ?v_54) (and (and (= x_41 1) (= x_31 x_40)) (= x_30 (not x_31))))) (= x_42 x_36)) (= x_4 x_0)) (= x_6 x_2)) (= x_27 x_26)) ?v_55))) (or (or (and (and (and (= x_43 0) ?v_61) (or (not (<= x_21 ?v_57)) (= x_42 x_31))) ?v_58) (and (and (and (= x_43 1) ?v_56) (xor x_31 x_30)) (= x_20 ?v_62))) (and (and (and (= x_43 2) ?v_56) (= x_31 x_30)) ?v_58))) (or (or (and (and (and (= x_44 0) (not ?v_59)) (or (not (<= x_25 ?v_52)) (= x_37 x_1))) ?v_60) (and (and (and (= x_44 1) ?v_59) (xor x_1 x_5)) (= x_24 (+ ?v_52 x_45)))) (and (and (and (= x_44 2) ?v_59) (= x_1 x_5)) ?v_60))) (or (or (and (and (and (= x_46 0) ?v_61) (or (not (<= x_29 ?v_57)) (= x_6 x_3))) ?v_64) (and (and (and (= x_46 1) ?v_56) (not ?v_63)) (= x_28 ?v_62))) (and (and (and (= x_46 2) ?v_56) ?v_63) ?v_64))) (xor x_97 x_98)) (not (= x_103 x_95)))))))))))
(check-sat)
(exit)
